\chapter{Introducción}
Recientemente se ha reconocido la importancia de poder caracterizar modelos de workflow (automatización parcial o total de un Proceso de Negocio) y propiedades de estos, de modo declarativo\cite{declDirk}. Se han propuesto numerosas herramientas que permiten expresar estas propiedades y permiten someter esta clase particular de modelos declarativos al análisis automático para la verificación de las mismas, por ejemplo la presentada en\cite{WestergaardMaggi2011}. Algunas herramientas de software realizan esta tarea mediante simulaciones de los modelos de workflow, mientras que otras realizan análisis de tipo estático.\\\newline
Este trabajo propone el uso de un tipo de lógica temporal conocida, fluent linear temporal logic\cite{GiannakopoulouMagee2003}, como medio para expresar propiedades sobre workflows de un modo flexible; así como el uso de un model checker para esta lógica que permite la verificación de las mismas sobre modelos procedurales de workflows. Creemos que esta lógica es mas apropiada que la lógica temporal lineal clásica a la hora de expresar propiedades sobre workflows. Los fluentes permiten expresar fácilmente propiedades relacionadas con la ejecución de tareas dentro de modelos de workflows. También permiten caracterizar de un modo sencillo estados abstractos del modelo, cuya caracterización sin fluentes, es decir, sólo con Linear Temporal Logic, se torna compleja e inmanejable.\\\newline
El desarrollo de herramientas de Software que plasmen las ideas y aportes de las ciencias ha sido uno de los pilares más importantes en los últimos tiempos para la difusión, colaboración y vinculación, no sólo, entre investigadores, sino también con la industria, como un modo de transferencia de conocimientos. Es por ello que se propone como objetivo integrador, el desarrollo de una herramienta de software, que denominamos \emph{FLWAnalizer} (Fluent Logic Workflow Analyzer), que brinde una guía tanto de investigación y estudio, como así también de aplicación de los conocimientos adquiridos durante la carrera. Esta herramienta permite analizar workflows por medio de la especificación y verificación de propiedades de comportamiento de los mismos.\\
Este trabajo se presenta de la siguiente manera: \\
El Capítulo 2 brinda una introducción a los temas que forman parte del trabajo, comenzando por una introducción a las Lógicas Temporales utilizadas para la caracterización de propiedades. Luego presenta un resumen de diferentes lenguajes para la descripción de Procesos de Negocios que permite al lector contextualizarse con el vocabulario y analizar objetivos comunes de los mismos. Finalmente introducimos el concepto de Sistema de Transición de Estados (LTS) y FSP, esta última es un álgebra de procesos que permite especificar LTSs de manera compacta. Estos formalismos serán utilizados como base para poder realizar el proceso de verificación. \\
En el capítulo 3 se tratarán los componentes que dieron origen a \emph{FLWAnaliyzer}. En este capítulo se caracterizará a \textit{YAWL} como lenguaje de modelado, luego se describirá una herramienta \textit{yawl2fsp} el cual va permitir la tracción de los modelos \textit{YAWL} en una lógica \textit{FSP} y por último \textit{LTSA} y \textit{DECLARE} dos herramientas que serán útiles en el momento de definir propiedades y el análisis y verificación de estas.\\
En en capítulo 4 se caracterizará los requerimientos de usuario, seguido por las funcionalidades necesarias para suplir dichas necesidades. Se continuará con el describiendo requerimientos por parte de las herramientas antes mencionadas.\\
En el capítulo 5 se detallará lo que representa el desarrollo y construcción de la herramienta de usuario siendo este el objetivo principal de este trabajo.\\
Finalmente en el capítulo 6 se realizará un detalle de un escenario utilizado para el desarrollo de este proyecto pasando por todas las etapas, es decir, desde el modelado hasta la definición de propiedades y la verificación de las mismas.